Nuprl Definition : R-icompat 11,40

R-icompat(AB)
== if Rplus?(A)
== ifthen R-icompat(Rplus-left(A); B R-icompat(Rplus-right(A); B)
== if Rplus?(B)
== ifthen R-icompat(A; Rplus-left(B))  R-icompat(A; Rplus-right(B))
== if Rnone?(A)
== ifthen True
== if Rnone?(B)
== ifthen True
== if eq_id(R-loc(A); R-loc(B))
== ifthen True
== else R-interface-compat(AB R-interface-compat(BA)
== fi 
(recursive) 
latex


DefinitionsR-interface-compat(AB), P  Q, True, R-loc(R), eq_id(ab), if b then t else f fi , Rnone?(x1), Rplus-right(x1), f(a), Rplus-left(x1), Rplus?(x1), x.A(x), Y
FDL editor aliasesR-icompat

origin